$\forall$$T$:Type, $L$:$T$ List, $P$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow\mathbb{B}$), $x$:$T$.
\\[0ex]($x$ $\in$ filter2($P$;$L$)) $\Leftrightarrow$ ($\exists$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $x$ $=$ $L$[$i$] \& $P$($i$))